<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>



<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.08">
<LINK rel="stylesheet" type="text/css" href="tutorial.css">
<TITLE>
Unification and Logical Variables
</TITLE>
</HEAD>
<BODY >
<A HREF="tutorial014.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="tutorial012.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="tutorial016.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
<HR>

<H2 CLASS="section"><A NAME="htoc29">3.3</A>&nbsp;&nbsp;Unification and Logical Variables</H2><UL>
<LI><A HREF="tutorial015.html#toc16">Symbolic Equality</A>
<LI><A HREF="tutorial015.html#toc17">Logical Variables</A>
<LI><A HREF="tutorial015.html#toc18">Unification</A>
</UL>

<A NAME="toc16"></A>
<H3 CLASS="subsection"><A NAME="htoc30">3.3.1</A>&nbsp;&nbsp;Symbolic Equality</H3>
<A NAME="@default52"></A>
Prolog has a particularly simple idea of <B>equality</B>, namely
structural equality by pattern matching. This means that two terms
are equal if and only if they have exactly the same structure. No
evaluation of any kind is perfomed on them:
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
?- 3 = 3.
Yes.
?- 3 = 4.
No.
?- hello = hello.
Yes.
?- hello = 3.
No.
?- foo(a,2) = foo(a,2).
Yes.
?- foo(a,2) = foo(b,2).
No.
?- foo(a,2) = foo(a,2,c).
No.
?- foo(3,4) = 7.
No.
?- +(3,4) = 7.
No.
?- 3 + 4 = 7.
No.
</PRE></BLOCKQUOTE>
Note in particular the last two examples (which are equivalent):
there is no automatic arithmetic evaluation. The term +(3,4) is simply
a data structure with two arguments, and therefore of course different from
any number.<BR>
<BR>
Note also that we have used the built-in predicate =/2, which exactly
implements this idea of equality.<BR>
<BR>
<A NAME="toc17"></A>
<H3 CLASS="subsection"><A NAME="htoc31">3.3.2</A>&nbsp;&nbsp;Logical Variables</H3>
<A NAME="@default53"></A>
<A NAME="@default54"></A> <A NAME="@default55"></A>
So far we have only performed tests, giving only Yes/No results.
How can we compute more interesting results? 
The solution is to introduce Logical Variables. 
It is very important to understand that Logical Variables are
variables in the mathematical sense, not in the usual programming
language sense. Logical Variables are simply placeholders for
values which are not yet known, like in mathematics.
In conventional programming languages on the other hand, variables
are labels for storage locations.
The important difference is that the value of a logical variables is
typically unknown at the beginning, and only becomes
known in the course of the computation. Once it is known, the variable is just
an alias for the value, i.e. it refers to a term.
Once a value has been assigned to a logical variable, it remains fixed
and cannot be assigned a different value. <BR>
<BR>
Logical Variables are written beginning with an upper-case letter or
an underscore, for example
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
X   Var   Quark   _123   R2D2
</PRE></BLOCKQUOTE>
If the same name occurs repeatedly in the same input term (e.g. the same
query or clause), it denotes the same variable.<BR>
<BR>
<A NAME="toc18"></A>
<H3 CLASS="subsection"><A NAME="htoc32">3.3.3</A>&nbsp;&nbsp;Unification</H3>
<A NAME="@default56"></A>
<A NAME="@default57"></A> <A NAME="@default58"></A> <A NAME="@default59"></A> <A NAME="@default60"></A>
With logical variables, the above equality tests become much more interesting,
resulting in the concept of <EM>Unification</EM>.
Unification is an extension of the idea of pattern matching of two terms.
In addition to matching, unification also causes the binding (instantiation,
aliasing) of variables in the two terms.
Unification instantiates variables such that the two unified terms become
equal. For example
<BLOCKQUOTE CLASS="quote"><PRE CLASS="verbatim">
X = 7                is true with X instantiated to 7
X = Y                is true with X aliased to Y (or vice versa)
foo(X) = foo(7)      is true with X instantiated to 7
foo(X,Y) = foo(3,4)  is true with X instantiated to 3 and Y to 4
foo(X,4) = foo(3,Y)  is true with X instantiated to 3 and Y to 4
foo(X) = foo(Y)      is true with X aliased to Y (or vice versa)
foo(X,X) = foo(3,4)  is false because there is no possible value for X
foo(X,4) = foo(3,X)  is false because there is no possible value for X
</PRE></BLOCKQUOTE>

	<BLOCKQUOTE CLASS="figure"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV>
	<DIV CLASS="center">
	<TABLE CELLPADDING=10>
<TR><TD BGCOLOR="#DB9370">
	
<DL CLASS="description" COMPACT=compact><DT CLASS="dt-description">
<B>Predicate</B><DD CLASS="dd-description"> Something that is true or false, depending on its definition
 and its arguments. Defines a relationship between its arguments.
<DT CLASS="dt-description"><B>Goal</B><DD CLASS="dd-description"> A logical formula whose truth value we want to know.
 A goal can be a conjunction or disjunction of other (sub-)goals.
<DT CLASS="dt-description"><B>Query</B><DD CLASS="dd-description"> The initial Goal given to a computation.
<DT CLASS="dt-description"><B>Unification</B><DD CLASS="dd-description"> An extension of pattern matching which can bind logical
 variables (placeholders) in the matched terms to make them equal.
<DT CLASS="dt-description"><B>Clause</B><DD CLASS="dd-description"> One alternative definition for when a predicate is true.
 A clause is logically an implication rule.
</DL>

	</TD>
</TR></TABLE>
	</DIV>
	<BR>
<BR>
<DIV CLASS="center">Figure 3.2: Basic Terminology</DIV><BR>
<BR>

	<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></BLOCKQUOTE>
<HR>
<A HREF="tutorial014.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="tutorial012.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="tutorial016.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
</BODY>
</HTML>
